w:World. FairFifo  (e:E, x:Id. state_when(e).x = (x when e)  vartype(loc(e);x)) 

latex

Definitions	t  T, x:A. B(x), P  Q, s.x, World, FairFifo, E, Id, state_when(e), <a, b>, , x:AB(x), s = t, loc(e), vartype(i;x)
Lemmas	Id wf, w-E wf, fair-fifo wf, world wf, w-when-lemma, subtype rel self, w-vartype wf, w-loc wf